M1, M2:MsgA. M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x)) 

latex

Definitions	x:A. B(x), P  Q, M.frame(k affects x), t.1, t.2, z != f(x)  P(a;z), t  T, , T, True, x. t(x), MsgA, M1  M2, Valtype(da;k), A c B, P & Q, f  g, x(s)
Lemmas	assert wf, squash wf, true wf, bool wf, deq-member wf, deq wf, Knd wf, Kind-deq wf, fpf-dom wf, Id wf, id-deq wf, fpf-trivial-subtype-top, ma-frame wf, ma-sub wf, msga wf